Termination w.r.t. Q proof of /tmp/tmpx7EScw/z082.srs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(c(a(x1))) → c(a(c(x1)))
a(a(b(x1))) → a(d(b(x1)))
a(b(x1)) → b(a(a(x1)))
d(d(x1)) → a(d(b(x1)))
b(b(x1)) → b(c(x1))
a(d(c(x1))) → c(a(x1))
b(c(x1)) → a(a(a(x1)))

Q is empty.

↳ QTRS

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

a(c(a(x1))) → c(a(c(x1)))
a(a(b(x1))) → a(d(b(x1)))
a(b(x1)) → b(a(a(x1)))
d(d(x1)) → a(d(b(x1)))
b(b(x1)) → b(c(x1))
a(d(c(x1))) → c(a(x1))
b(c(x1)) → a(a(a(x1)))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

a(c(a(x1))) → c(a(c(x1)))
a(a(b(x1))) → a(d(b(x1)))
a(b(x1)) → b(a(a(x1)))
d(d(x1)) → a(d(b(x1)))
b(b(x1)) → b(c(x1))
a(d(c(x1))) → c(a(x1))
b(c(x1)) → a(a(a(x1)))

The set Q is empty.
We have obtained the following QTRS:

a(c(a(x))) → c(a(c(x)))
b(a(a(x))) → b(d(a(x)))
b(a(x)) → a(a(b(x)))
d(d(x)) → b(d(a(x)))
b(b(x)) → c(b(x))
c(d(a(x))) → a(c(x))
c(b(x)) → a(a(a(x)))

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

    ↳ QTRS

      ↳ RFCMatchBoundsTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a(c(a(x))) → c(a(c(x)))
b(a(a(x))) → b(d(a(x)))
b(a(x)) → a(a(b(x)))
d(d(x)) → b(d(a(x)))
b(b(x)) → c(b(x))
c(d(a(x))) → a(c(x))
c(b(x)) → a(a(a(x)))

Q is empty.

Termination of the TRS R could be shown with a Match Bound [6,7] of 4. This implies Q-termination of R.
The following rules were used to construct the certificate:

a(c(a(x))) → c(a(c(x)))
b(a(a(x))) → b(d(a(x)))
b(a(x)) → a(a(b(x)))
d(d(x)) → b(d(a(x)))
b(b(x)) → c(b(x))
c(d(a(x))) → a(c(x))
c(b(x)) → a(a(a(x)))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

108, 109, 110, 112, 111, 113, 114, 115, 117, 116, 119, 118, 120, 121, 123, 122, 125, 124, 127, 126, 129, 128, 131, 130, 133, 132, 135, 134, 137, 136, 139, 138, 141, 140, 143, 142, 145, 144, 168, 167

Node 108 is start node and node 109 is final node.

Those nodes are connect through the following edges:

108 to 110 labelled a_1(0), c_1(1)
108 to 111 labelled a_1(0)
108 to 113 labelled b_1(0)
108 to 108 labelled c_1(0)
108 to 112 labelled c_1(0)
108 to 122 labelled a_1(1)
108 to 116 labelled a_1(1)
108 to 126 labelled c_1(1)
108 to 134 labelled c_1(2)
109 to 109 labelled #_1(0)
110 to 109 labelled c_1(0)
110 to 115 labelled a_1(1)
110 to 116 labelled a_1(1)
110 to 110 labelled c_1(1)
110 to 128 labelled c_1(2)
110 to 134 labelled c_1(2)
112 to 109 labelled b_1(0), a_1(0)
112 to 118 labelled a_1(1)
112 to 120 labelled b_1(1)
112 to 119 labelled c_1(1)
112 to 110 labelled c_1(1)
112 to 124 labelled a_1(2)
112 to 136 labelled c_1(2)
112 to 138 labelled c_1(3)
111 to 112 labelled a_1(0)
111 to 126 labelled c_1(1)
113 to 114 labelled d_1(0)
114 to 109 labelled a_1(0)
114 to 110 labelled c_1(1)
115 to 109 labelled c_1(1)
115 to 115 labelled a_1(1)
115 to 116 labelled a_1(1)
115 to 110 labelled c_1(1)
115 to 127 labelled c_1(1)
115 to 128 labelled c_1(2)
115 to 134 labelled c_1(2)
115 to 129 labelled c_1(1)
115 to 135 labelled c_1(1)
117 to 109 labelled a_1(1)
117 to 110 labelled c_1(1)
117 to 120 labelled a_1(1)
116 to 117 labelled a_1(1)
116 to 128 labelled c_1(2)
119 to 109 labelled b_1(1)
119 to 118 labelled a_1(1)
119 to 120 labelled b_1(1)
119 to 119 labelled c_1(1)
119 to 124 labelled a_1(2)
119 to 136 labelled c_1(2)
119 to 138 labelled c_1(3)
118 to 119 labelled a_1(1)
118 to 130 labelled c_1(2)
120 to 121 labelled d_1(1)
121 to 109 labelled a_1(1)
121 to 110 labelled c_1(1)
123 to 113 labelled a_1(1)
122 to 123 labelled a_1(1)
125 to 109 labelled a_1(2)
125 to 120 labelled a_1(2)
125 to 110 labelled c_1(1)
124 to 125 labelled a_1(2)
124 to 128 labelled c_1(2)
127 to 116 labelled c_1(1)
127 to 115 labelled c_1(1)
127 to 118 labelled c_1(1)
127 to 124 labelled c_1(1)
127 to 137 labelled c_1(1)
127 to 139 labelled c_1(1)
126 to 127 labelled a_1(1)
126 to 128 labelled c_1(2)
126 to 132 labelled c_1(2)
129 to 116 labelled c_1(2), a_1(1)
129 to 115 labelled c_1(2), a_1(1)
129 to 117 labelled c_1(2)
129 to 109 labelled c_1(2)
129 to 120 labelled c_1(2)
129 to 129 labelled a_1(2)
129 to 125 labelled c_1(2)
129 to 135 labelled c_1(2)
129 to 110 labelled c_1(1)
129 to 128 labelled c_1(2)
129 to 134 labelled c_1(2)
129 to 144 labelled c_1(3)
129 to 138 labelled c_1(3)
129 to 142 labelled c_1(3)
128 to 129 labelled a_1(2)
128 to 128 labelled c_1(2)
128 to 110 labelled c_1(1)
128 to 144 labelled c_1(3)
128 to 138 labelled c_1(3)
128 to 142 labelled c_1(3)
131 to 118 labelled c_1(2)
131 to 124 labelled c_1(2)
131 to 137 labelled c_1(2)
131 to 139 labelled c_1(2)
130 to 131 labelled a_1(2)
130 to 132 labelled c_1(2)
130 to 140 labelled c_1(3)
133 to 119 labelled c_1(2)
133 to 124 labelled a_1(2)
133 to 138 labelled c_1(3)
132 to 133 labelled a_1(2)
132 to 130 labelled c_1(2)
132 to 142 labelled c_1(3)
135 to 129 labelled c_1(2)
134 to 135 labelled a_1(2)
134 to 128 labelled c_1(2)
134 to 138 labelled c_1(3)
137 to 131 labelled c_1(2)
136 to 137 labelled a_1(2)
139 to 129 labelled c_1(3)
139 to 135 labelled c_1(3)
139 to 145 labelled c_1(3)
139 to 143 labelled c_1(3)
138 to 139 labelled a_1(3)
138 to 128 labelled c_1(2)
138 to 138 labelled c_1(3)
141 to 125 labelled c_1(3)
140 to 141 labelled a_1(3)
140 to 144 labelled c_1(3)
143 to 124 labelled c_1(3)
143 to 139 labelled c_1(3)
142 to 143 labelled a_1(3)
142 to 140 labelled c_1(3)
145 to 109 labelled c_1(3)
145 to 120 labelled c_1(3)
145 to 115 labelled a_1(1)
145 to 116 labelled a_1(1)
145 to 129 labelled a_1(2)
145 to 128 labelled c_1(2)
145 to 144 labelled c_1(3)
145 to 134 labelled c_1(2)
145 to 138 labelled c_1(3)
145 to 142 labelled c_1(3)
145 to 110 labelled c_1(1)
144 to 145 labelled a_1(3)
144 to 110 labelled c_1(1)
144 to 128 labelled c_1(2)
144 to 138 labelled c_1(3)
144 to 167 labelled c_1(4)
168 to 145 labelled c_1(4)
168 to 139 labelled c_1(4)
168 to 143 labelled c_1(4)
167 to 168 labelled a_1(4)
167 to 128 labelled c_1(2)
167 to 138 labelled c_1(3)